;;; -*- Mode: Lisp; Package: STELLA; Syntax: COMMON-LISP; Base: 10 -*-

(CL:IN-PACKAGE "STELLA")

(IN-MODULE "/PL-KERNEL-KB/PL-FOUNDATION")

(IN-DIALECT :KIF)

;------------------------------------------------------------------------------
; Basic Definitions
;------------------------------------------------------------------------------

(ASSERT (Being Being_Empty))
(ASSERT (Being Universe))

;------------------------------------------------------------------------------
; Function Definitions
;------------------------------------------------------------------------------

(DEFFUNCTION sum  ((?b1 Being) (?b2 Being)) :-> (?b3 Being))
(DEFFUNCTION isc  ((?b1 Being) (?b2 Being)) :-> (?b3 Being))
(DEFFUNCTION cpl  ((?b1 Being)) :-> (?b2 Being))

;------------------------------------------------------------------------------
; Set Rules
;------------------------------------------------------------------------------

(ASSERT (
    FORALL ((?b1 Being))
        (AND
            ( sum ?b1 ?b1 ?b1 )
            ( isc ?b1 ?b1 ?b1 )
            
            ( sum ?b1 Being_Empty ?b1 )
            ( isc ?b1 Being_Empty Being_Empty )
            ( sum ?b1 Universe Universe )
            ( isc ?b1 Universe ?b1 )
            
            ( cpl (cpl ?b1) ?b1 )
            ( sum ?b1 (cpl ?b1) Universe )
            ( isc ?b1 (cpl ?b1) Being_Empty )
        )
))

(ASSERT (
    FORALL ((?b1 Being) (?b2 Being))
        (AND
            ( sum ?b1 ?b2 (sum ?b2 ?b1) )
            ( isc ?b1 ?b2 (isc ?b2 ?b1) )

            ( cpl (sum ?b1 ?b2) (isc (cpl ?b1) (cpl ?b2)) )
            ( cpl (isc ?b1 ?b2) (sum (cpl ?b1) (cpl ?b2)) )
        )
))

(ASSERT (
    FORALL ((?b1 Being) (?b2 Being) (?b3 Being))
        (AND
            ( sum (sum ?b1 ?b2) ?b3 (sum ?b1 (sum ?b2 ?b3)) )
            ( isc (isc ?b1 ?b2) ?b3 (isc ?b1 (isc ?b2 ?b3)) )

            ( isc ?b1 (sum ?b2 ?b3) (sum (isc ?b1 ?b2) (isc ?b1 ?b3)) )

            ( sum ?b1 (isc ?b2 ?b3) (isc (sum ?b1 ?b2) (sum ?b1 ?b3)) )
        )
))